(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
head(Cons(x, xs)) → x
factor(Cons(RPar, xs)) → xs
factor(Cons(Div, xs)) → xs
factor(Cons(Mul, xs)) → xs
factor(Cons(Plus, xs)) → xs
factor(Cons(Minus, xs)) → xs
factor(Cons(Val(int), xs)) → xs
factor(Cons(LPar, xs)) → factor[Ite][True][Let](Cons(LPar, xs), expr(Cons(LPar, xs)))
member(x', Cons(x, xs)) → member[Ite][True][Ite](eqAlph(x, x'), x', Cons(x, xs))
member(x, Nil) → False
atom(Cons(x, xs)) → xs
atom(Nil) → Nil
eqAlph(RPar, RPar) → True
eqAlph(RPar, LPar) → False
eqAlph(RPar, Div) → False
eqAlph(RPar, Mul) → False
eqAlph(RPar, Plus) → False
eqAlph(RPar, Minus) → False
eqAlph(RPar, Val(int2)) → False
eqAlph(LPar, RPar) → False
eqAlph(LPar, LPar) → True
eqAlph(LPar, Div) → False
eqAlph(LPar, Mul) → False
eqAlph(LPar, Plus) → False
eqAlph(LPar, Minus) → False
eqAlph(LPar, Val(int2)) → False
eqAlph(Div, RPar) → False
eqAlph(Div, LPar) → False
eqAlph(Div, Div) → True
eqAlph(Div, Mul) → False
eqAlph(Div, Plus) → False
eqAlph(Div, Minus) → False
eqAlph(Div, Val(int2)) → False
eqAlph(Mul, RPar) → False
eqAlph(Mul, LPar) → False
eqAlph(Mul, Div) → False
eqAlph(Mul, Mul) → True
eqAlph(Mul, Plus) → False
eqAlph(Mul, Minus) → False
eqAlph(Mul, Val(int2)) → False
eqAlph(Plus, RPar) → False
eqAlph(Plus, LPar) → False
eqAlph(Plus, Div) → False
eqAlph(Plus, Mul) → False
eqAlph(Plus, Plus) → True
eqAlph(Plus, Minus) → False
eqAlph(Plus, Val(int2)) → False
eqAlph(Minus, RPar) → False
eqAlph(Minus, LPar) → False
eqAlph(Minus, Div) → False
eqAlph(Minus, Mul) → False
eqAlph(Minus, Plus) → False
eqAlph(Minus, Minus) → True
eqAlph(Minus, Val(int2)) → False
eqAlph(Val(int), RPar) → False
eqAlph(Val(int), LPar) → False
eqAlph(Val(int), Div) → False
eqAlph(Val(int), Mul) → False
eqAlph(Val(int), Plus) → False
eqAlph(Val(int), Minus) → False
eqAlph(Val(int), Val(int2)) → !EQ(int2, int)
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
term(xs) → term[Let](xs, factor(xs))
parsexp(xs) → expr(xs)
expr(xs) → expr[Let](xs, term(xs))
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
factor[Ite][True][Let](xs', Cons(RPar, xs)) → factor[Ite][True][Let][Ite](True, xs', Cons(RPar, xs))
factor[Ite][True][Let](xs', Cons(LPar, xs)) → factor[Ite][True][Let][Ite](False, xs', Cons(LPar, xs))
factor[Ite][True][Let](xs', Cons(Div, xs)) → factor[Ite][True][Let][Ite](False, xs', Cons(Div, xs))
factor[Ite][True][Let](xs', Cons(Mul, xs)) → factor[Ite][True][Let][Ite](False, xs', Cons(Mul, xs))
factor[Ite][True][Let](xs', Cons(Plus, xs)) → factor[Ite][True][Let][Ite](False, xs', Cons(Plus, xs))
factor[Ite][True][Let](xs', Cons(Minus, xs)) → factor[Ite][True][Let][Ite](False, xs', Cons(Minus, xs))
factor[Ite][True][Let](xs', Cons(Val(int), xs)) → factor[Ite][True][Let][Ite](False, xs', Cons(Val(int), xs))
term[Let](xs', Cons(x, xs)) → term[Let][Ite][False][Ite](member(x, Cons(Mul, Cons(Div, Nil))), xs', Cons(x, xs))
expr[Let](xs', Cons(x, xs)) → expr[Let][Ite][False][Ite](member(x, Cons(Plus, Cons(Minus, Nil))), xs', Cons(x, xs))
term[Let](xs, Nil) → Nil
member[Ite][True][Ite](False, x', Cons(x, xs)) → member(x', xs)
factor[Ite][True][Let](xs, Nil) → factor[Ite][True][Let][Ite](and(False, eqAlph(head(Nil), RPar)), xs, Nil)
expr[Let](xs, Nil) → Nil
member[Ite][True][Ite](True, x, xs) → True
Rewrite Strategy: INNERMOST
(1) InfiniteLowerBoundProof (EQUIVALENT transformation)
The loop following loop proves infinite runtime complexity:
The rewrite sequence
factor(Cons(LPar, xs)) →+ factor[Ite][True][Let](Cons(LPar, xs), expr[Let](Cons(LPar, xs), term[Let](Cons(LPar, xs), factor(Cons(LPar, xs)))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1,1,1].
The pumping substitution is [ ].
The result substitution is [ ].
(2) BOUNDS(INF, INF)